One of the most challenging problems in deductive program verification is to find inductive program invariants. Typically, program verifiers require inductive invariants in order to establish correctness proofs. However, stand-alone theorem provers have been unable to find such invariants and require additional support from either a person doing the program verification, or additional tools that can extract auxiliary program invariants. Often, auxiliary invariants state properties about a large collection of values. Such statements can be represented compactly using quantifiers.
While quantifiers enable program verifiers, they are only conceptual constructs and are not executable. This is a problem when testing a program, e.g., to quickly detect errors (as opposed to proving a program correct). Checking code contracts with quantifiers efficiently is particularly challenging because test cases should limit themselves to only unfold quantifiers on a limited set of values in order to be effective.
For example, if a contract ensures that an array with 1 million entries be initialized with a fixed value, then a test program may choose to check that the array is indeed initialized with the same value on all entries. However, if a program only touches the array in two entries, it is much more effective to only check the contract on two representative entries that are affected.
Broadly speaking, many modern specification and verification systems such as Spec#, the Java Modeling language (JML) and so forth, use a design-by-contract approach where the specification language is typically an extension of the underlying programming language. The verification of contracts often uses verification condition generation (VCG). The verification conditions are first-order logical formulas whose validity implies the correctness of the program. The formulas are then fed to interactive or automatic theorem provers.
In practice, there are two limitations of the VCG and proving approach. First, most program verification tools do not by themselves produce sufficiently strong contracts. Such contracts need to be crafted or synthesized independently, usually by a human being. Second, if the program verification tool fails to prove the desired properties, then discovering the mismatch between the contracts and the code, or why the contracts were not strong enough, remains a difficult task. In practice, the program verification tools offer limited help.
Most program verification tools employ an automated solver to prove program properties. These solvers must typically be able to handle a combination of domains, such as integers, bit-vectors, arrays, heaps, and data-types, which are often found in programming languages. In addition, most contracts of interest involve functional correctness and the program's heap. These contracts often involve quantifiers, which solvers must reason about.
One type of solvers that combine various theories is known as a Satisfiability Modulo Theories solver or SMT solver. SMT solvers have recently gained substantial attention. To support quantifiers, one technique used in SMT solvers is pattern matching to determine relevant quantifier instantiations. Pattern matching happens inside of the solver on top of the generated verification condition.
When a proof attempt fails, pin-pointing any insufficient annotation within the context of the SMT solver is obscured by the indirection from the program itself. To give good feedback to a developer in such a case, the SMT solver should provide a human-readable counter-example, i.e. a model of the failed proof attempt. However, producing informative models from quantified formulas remains an open research challenge.